(PROOF ONE) 
1 	(ASS (IMPLIES X (IMPLIES Y Z)))
2 	(ASS (IMPLIES X (IMPLIES Z Y)))
3 	(ASS Y)
4 	(ASS (NOT Z))
5 	(ASS X)
6 	(MP 5 1)
7 	(MP 3 6)
8 	(AI 4 7)
9 	(TAUT NIL 8)
10 	(ASS (NOT X))
11 	(DED 9 4 3 5 1)
12 	(TAUT FALSE 8)
13 	(DED 12 4 3 5 1)
14 	(NI 13)
15 	(TAUT (OR Z (NOT Y) (NOT X) (NOT (IMPLIES X (IMPLIES Y Z))))
	      14)
16 	(TAUT (IMPLIES (AND Y (NOT Z) (IMPLIES X (IMPLIES Y Z)))
		       (NOT X))
	      15)
(MAKETHM HI 15 ONE)


17 	(USETHM HI)
18 	(UG 17 Z X)
19 	(EG 18 Y)
20 	(US 18 X)
21 	(US 19 X)

(PROOF VALUE) 
(MAKETHM HI 15 ONE)